effect_p(es; i; ds; k; T; x; f)
== ((x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
==  subtype_rel(es-kindtype(es; i; k); T))
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.((es-kind(es; e) = k)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (es_state_after(es; e)(x) = f(es-state-when(es; e),es-val(es; e)))))) 

latex

---

clarification:

effect_p(es; i; ds; k; T; x; f)
== ((x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
==  subtype_rel(es-kindtype(es; i; k); T))
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.((es-kind(es; e) = k  Knd)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (es_state_after(es; e)(x)
== c alle-at( c (=
== c alle-at( c (f(es-state-when(es; e),es-val(es; e))
== c alle-at( c ( rationalsfpf-cap(ds; id-deq; x; top))))) 

latex

Definitions	P  Q, x:A. B(x), Id, es-vartype(es; i; x), es-kindtype(es; i; k), alle-at(es; i; e.P(e)), P  Q, Knd, es-kind(es; e), A c B, es-valtype(es; e), s = t, x:AB(x), rationals, fpf-cap(f; eq; x; z), id-deq, top, es_state_after(es; e), f(a), es-state-when(es; e), es-val(es; e)
FDL editor aliases	effect_p